Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    a__fact(X)  → a__if(a__zero(mark(X)),s(0),prod(X,fact(p(X))))
2:    a__add(0,X)  → mark(X)
3:    a__add(s(X),Y)  → s(a__add(mark(X),mark(Y)))
4:    a__prod(0,X)  → 0
5:    a__prod(s(X),Y)  → a__add(mark(Y),a__prod(mark(X),mark(Y)))
6:    a__if(true,X,Y)  → mark(X)
7:    a__if(false,X,Y)  → mark(Y)
8:    a__zero(0)  → true
9:    a__zero(s(X))  → false
10:    a__p(s(X))  → mark(X)
11:    mark(fact(X))  → a__fact(mark(X))
12:    mark(if(X1,X2,X3))  → a__if(mark(X1),X2,X3)
13:    mark(zero(X))  → a__zero(mark(X))
14:    mark(prod(X1,X2))  → a__prod(mark(X1),mark(X2))
15:    mark(p(X))  → a__p(mark(X))
16:    mark(add(X1,X2))  → a__add(mark(X1),mark(X2))
17:    mark(s(X))  → s(mark(X))
18:    mark(0)  → 0
19:    mark(true)  → true
20:    mark(false)  → false
21:    a__fact(X)  → fact(X)
22:    a__if(X1,X2,X3)  → if(X1,X2,X3)
23:    a__zero(X)  → zero(X)
24:    a__prod(X1,X2)  → prod(X1,X2)
25:    a__p(X)  → p(X)
26:    a__add(X1,X2)  → add(X1,X2)
There are 29 dependency pairs:
27:    A__FACT(X)  → A__IF(a__zero(mark(X)),s(0),prod(X,fact(p(X))))
28:    A__FACT(X)  → A__ZERO(mark(X))
29:    A__FACT(X)  → MARK(X)
30:    A__ADD(0,X)  → MARK(X)
31:    A__ADD(s(X),Y)  → A__ADD(mark(X),mark(Y))
32:    A__ADD(s(X),Y)  → MARK(X)
33:    A__ADD(s(X),Y)  → MARK(Y)
34:    A__PROD(s(X),Y)  → A__ADD(mark(Y),a__prod(mark(X),mark(Y)))
35:    A__PROD(s(X),Y)  → A__PROD(mark(X),mark(Y))
36:    A__PROD(s(X),Y)  → MARK(X)
37:    A__PROD(s(X),Y)  → MARK(Y)
38:    A__IF(true,X,Y)  → MARK(X)
39:    A__IF(false,X,Y)  → MARK(Y)
40:    A__P(s(X))  → MARK(X)
41:    MARK(fact(X))  → A__FACT(mark(X))
42:    MARK(fact(X))  → MARK(X)
43:    MARK(if(X1,X2,X3))  → A__IF(mark(X1),X2,X3)
44:    MARK(if(X1,X2,X3))  → MARK(X1)
45:    MARK(zero(X))  → A__ZERO(mark(X))
46:    MARK(zero(X))  → MARK(X)
47:    MARK(prod(X1,X2))  → A__PROD(mark(X1),mark(X2))
48:    MARK(prod(X1,X2))  → MARK(X1)
49:    MARK(prod(X1,X2))  → MARK(X2)
50:    MARK(p(X))  → A__P(mark(X))
51:    MARK(p(X))  → MARK(X)
52:    MARK(add(X1,X2))  → A__ADD(mark(X1),mark(X2))
53:    MARK(add(X1,X2))  → MARK(X1)
54:    MARK(add(X1,X2))  → MARK(X2)
55:    MARK(s(X))  → MARK(X)
The approximated dependency graph contains one SCC: {27,29-44,46-55}.
Tyrolean Termination Tool  (26.55 seconds)   ---  May 3, 2006